Termination Proof Script
Consider the TRS R consisting of the rewrite rules
1:
not
(x)
→
xor
(x,
true
)
2:
implies
(x,y)
→
xor
(
and
(x,y),
xor
(x,
true
))
3:
or
(x,y)
→
xor
(
and
(x,y),
xor
(x,y))
4:
x
=
y
→
xor
(x,
xor
(y,
true
))
There are no dependency pairs. Hence the TRS is trivially terminating.
Tyrolean Termination Tool
(0.01 seconds) --- May 3, 2006